[−][src]Crate boolector_sys

Low-level bindings for the Boolector SMT solver.

Please see the Boolector C API documentation for function descriptions.

Re-exports

pub use self::BtorOptQuantSynth as BtorOptQuantSynt;

Structs

BoolectorAnonymous
BoolectorNode
Btor
BtorAbortCallback
BtorNode

Constants

BTOR_BETA_REDUCE_ALL
BTOR_BETA_REDUCE_FUN
BTOR_BETA_REDUCE_NONE
BTOR_DP_QSORT_ASC
BTOR_DP_QSORT_DESC
BTOR_DP_QSORT_JUST
BTOR_ENGINE_AIGPROP
BTOR_ENGINE_FUN
BTOR_ENGINE_PROP
BTOR_ENGINE_QUANT
BTOR_ENGINE_SLS
BTOR_FUN_EAGER_LEMMAS_ALL
BTOR_FUN_EAGER_LEMMAS_CONF
BTOR_FUN_EAGER_LEMMAS_NONE
BTOR_INCREMENTAL_SMT1_BASIC
BTOR_INCREMENTAL_SMT1_CONTINUE
BTOR_INPUT_FORMAT_BTOR
BTOR_INPUT_FORMAT_BTOR2
BTOR_INPUT_FORMAT_NONE
BTOR_INPUT_FORMAT_SMT1
BTOR_INPUT_FORMAT_SMT2
BTOR_JUST_HEUR_BRANCH_LEFT
BTOR_JUST_HEUR_BRANCH_MIN_APP
BTOR_JUST_HEUR_BRANCH_MIN_DEP
BTOR_OPT_ACKERMANN
BTOR_OPT_AIGPROP_USE_BANDIT
BTOR_OPT_AIGPROP_USE_RESTARTS
BTOR_OPT_AUTO_CLEANUP
BTOR_OPT_AUTO_CLEANUP_INTERNAL
BTOR_OPT_BETA_REDUCE
BTOR_OPT_CHK_FAILED_ASSUMPTIONS
BTOR_OPT_CHK_MODEL
BTOR_OPT_CHK_UNCONSTRAINED
BTOR_OPT_DECLSORT_BV_WIDTH
BTOR_OPT_ELIMINATE_SLICES
BTOR_OPT_ENGINE
BTOR_OPT_EXIT_CODES
BTOR_OPT_EXTRACT_LAMBDAS
BTOR_OPT_FUN_DUAL_PROP
BTOR_OPT_FUN_DUAL_PROP_QSORT
BTOR_OPT_FUN_EAGER_LEMMAS
BTOR_OPT_FUN_JUST
BTOR_OPT_FUN_JUST_HEURISTIC
BTOR_OPT_FUN_LAZY_SYNTHESIZE
BTOR_OPT_FUN_PREPROP
BTOR_OPT_FUN_PRESLS
BTOR_OPT_FUN_STORE_LAMBDAS
BTOR_OPT_INCREMENTAL
BTOR_OPT_INCREMENTAL_SMT1
BTOR_OPT_INPUT_FORMAT
BTOR_OPT_LOGLEVEL
BTOR_OPT_MERGE_LAMBDAS
BTOR_OPT_MODEL_GEN
BTOR_OPT_NONDESTR_SUBST
BTOR_OPT_NORMALIZE
BTOR_OPT_NORMALIZE_ADD
BTOR_OPT_NUM_OPTS
BTOR_OPT_OUTPUT_FORMAT
BTOR_OPT_OUTPUT_NUMBER_FORMAT
BTOR_OPT_PARSE_INTERACTIVE
BTOR_OPT_PRETTY_PRINT
BTOR_OPT_PRINT_DIMACS
BTOR_OPT_PROP_FLIP_COND_CONST_DELTA
BTOR_OPT_PROP_FLIP_COND_CONST_NPATHSEL
BTOR_OPT_PROP_NO_MOVE_ON_CONFLICT
BTOR_OPT_PROP_NPROPS
BTOR_OPT_PROP_PATH_SEL
BTOR_OPT_PROP_PROB_AND_FLIP
BTOR_OPT_PROP_PROB_CONC_FLIP
BTOR_OPT_PROP_PROB_EQ_FLIP
BTOR_OPT_PROP_PROB_FLIP_COND
BTOR_OPT_PROP_PROB_FLIP_COND_CONST
BTOR_OPT_PROP_PROB_SLICE_FLIP
BTOR_OPT_PROP_PROB_SLICE_KEEP_DC
BTOR_OPT_PROP_PROB_USE_INV_VALUE
BTOR_OPT_PROP_USE_BANDIT
BTOR_OPT_PROP_USE_RESTARTS
BTOR_OPT_QUANT_CER
BTOR_OPT_QUANT_DER
BTOR_OPT_QUANT_DUAL_SOLVER
BTOR_OPT_QUANT_FIXSYNTH
BTOR_OPT_QUANT_MINISCOPE
BTOR_OPT_QUANT_SYNTH
BTOR_OPT_QUANT_SYNTH_ITE_COMPLETE
BTOR_OPT_QUANT_SYNTH_LIMIT
BTOR_OPT_QUANT_SYNTH_QI
BTOR_OPT_REWRITE_LEVEL
BTOR_OPT_RW_ZERO_LOWER_SLICE
BTOR_OPT_SAT_ENGINE
BTOR_OPT_SAT_ENGINE_CADICAL_FREEZE
BTOR_OPT_SAT_ENGINE_LGL_FORK
BTOR_OPT_SAT_ENGINE_N_THREADS
BTOR_OPT_SEED
BTOR_OPT_SIMPLIFY_CONSTRAINTS
BTOR_OPT_SIMP_NORMAMLIZE_ADDERS
BTOR_OPT_SKELETON_PREPROC
BTOR_OPT_SLS_JUST
BTOR_OPT_SLS_MOVE_GW
BTOR_OPT_SLS_MOVE_INC_MOVE_TEST
BTOR_OPT_SLS_MOVE_PROP
BTOR_OPT_SLS_MOVE_PROP_FORCE_RW
BTOR_OPT_SLS_MOVE_PROP_N_PROP
BTOR_OPT_SLS_MOVE_PROP_N_SLS
BTOR_OPT_SLS_MOVE_RAND_ALL
BTOR_OPT_SLS_MOVE_RAND_RANGE
BTOR_OPT_SLS_MOVE_RAND_WALK
BTOR_OPT_SLS_MOVE_RANGE
BTOR_OPT_SLS_MOVE_SEGMENT
BTOR_OPT_SLS_NFLIPS
BTOR_OPT_SLS_PROB_MOVE_RAND_WALK
BTOR_OPT_SLS_STRATEGY
BTOR_OPT_SLS_USE_BANDIT
BTOR_OPT_SLS_USE_RESTARTS
BTOR_OPT_SORT_AIG
BTOR_OPT_SORT_AIGVEC
BTOR_OPT_SORT_EXP
BTOR_OPT_UCOPT
BTOR_OPT_VAR_SUBST
BTOR_OPT_VERBOSITY
BTOR_OUTPUT_BASE_BIN
BTOR_OUTPUT_BASE_DEC
BTOR_OUTPUT_BASE_HEX
BTOR_OUTPUT_FORMAT_AIGER_ASCII
BTOR_OUTPUT_FORMAT_AIGER_BINARY
BTOR_OUTPUT_FORMAT_BTOR
BTOR_OUTPUT_FORMAT_NONE
BTOR_OUTPUT_FORMAT_SMT2
BTOR_PROP_PATH_SEL_CONTROLLING
BTOR_PROP_PATH_SEL_ESSENTIAL
BTOR_PROP_PATH_SEL_RANDOM
BTOR_QUANT_SYNTH_EL
BTOR_QUANT_SYNTH_ELMC
BTOR_QUANT_SYNTH_ELMR
BTOR_QUANT_SYNTH_EL_ELMC
BTOR_QUANT_SYNTH_NONE
BTOR_SAT_ENGINE_CADICAL
BTOR_SAT_ENGINE_CMS
BTOR_SAT_ENGINE_LINGELING
BTOR_SAT_ENGINE_MINISAT
BTOR_SAT_ENGINE_PICOSAT
BTOR_SLS_STRAT_ALWAYS_PROP
BTOR_SLS_STRAT_BEST_MOVE
BTOR_SLS_STRAT_BEST_SAME_MOVE
BTOR_SLS_STRAT_FIRST_BEST_MOVE
BTOR_SLS_STRAT_RAND_WALK
BtorSolverResult_BTOR_RESULT_SAT
BtorSolverResult_BTOR_RESULT_UNKNOWN
BtorSolverResult_BTOR_RESULT_UNSAT

Functions

boolector_add ^⚠
boolector_and ^⚠
boolector_apply ^⚠
boolector_array ^⚠
boolector_array_assignment ^⚠
boolector_array_sort ^⚠
boolector_assert ^⚠
boolector_assume ^⚠
boolector_bitvec_sort ^⚠
boolector_bitvec_sort_get_width ^⚠
boolector_bool_sort ^⚠
boolector_bv_assignment ^⚠
boolector_clone ^⚠
boolector_concat ^⚠
boolector_cond ^⚠
boolector_const ^⚠
boolector_const_array ^⚠
boolector_constd ^⚠
boolector_consth ^⚠
boolector_copy ^⚠
boolector_copy_sort ^⚠
boolector_copyright ^⚠
boolector_dec ^⚠
boolector_delete ^⚠
boolector_dump_aiger_ascii ^⚠
boolector_dump_aiger_binary ^⚠
boolector_dump_btor ^⚠
boolector_dump_btor_node ^⚠
boolector_dump_smt2 ^⚠
boolector_dump_smt2_node ^⚠
boolector_eq ^⚠
boolector_exists ^⚠
boolector_failed ^⚠
boolector_false ^⚠
boolector_first_opt ^⚠
boolector_fixate_assumptions ^⚠
boolector_forall ^⚠
boolector_free_array_assignment ^⚠
boolector_free_bits ^⚠
boolector_free_bv_assignment ^⚠
boolector_free_uf_assignment ^⚠
boolector_fun ^⚠
boolector_fun_get_codomain_sort ^⚠
boolector_fun_get_domain_sort ^⚠
boolector_fun_sort ^⚠
boolector_fun_sort_check ^⚠
boolector_get_bits ^⚠
boolector_get_btor ^⚠
boolector_get_failed_assumptions ^⚠
boolector_get_fun_arity ^⚠
boolector_get_index_width ^⚠
boolector_get_node_id ^⚠
boolector_get_opt ^⚠
boolector_get_opt_desc ^⚠
boolector_get_opt_dflt ^⚠
boolector_get_opt_lng ^⚠
boolector_get_opt_max ^⚠
boolector_get_opt_min ^⚠
boolector_get_opt_shrt ^⚠
boolector_get_refs ^⚠
boolector_get_sort ^⚠
boolector_get_symbol ^⚠
boolector_get_trapi ^⚠
boolector_get_width ^⚠
boolector_git_id ^⚠
boolector_has_opt ^⚠
boolector_iff ^⚠
boolector_implies ^⚠
boolector_inc ^⚠
boolector_int ^⚠
boolector_is_array ^⚠
boolector_is_array_sort ^⚠
boolector_is_array_var ^⚠
boolector_is_bitvec_sort ^⚠
boolector_is_bound_param ^⚠
boolector_is_bv_const_max_signed ^⚠
boolector_is_bv_const_min_signed ^⚠
boolector_is_bv_const_one ^⚠
boolector_is_bv_const_ones ^⚠
boolector_is_bv_const_zero ^⚠
boolector_is_const ^⚠
boolector_is_equal_sort ^⚠
boolector_is_fun ^⚠
boolector_is_fun_sort ^⚠
boolector_is_param ^⚠
boolector_is_uf ^⚠
boolector_is_var ^⚠
boolector_limited_sat ^⚠
boolector_match_node ^⚠
boolector_match_node_by_id ^⚠
boolector_match_node_by_symbol ^⚠
boolector_max_signed ^⚠
boolector_min_signed ^⚠
boolector_mul ^⚠
boolector_nand ^⚠
boolector_ne ^⚠
boolector_neg ^⚠
boolector_new ^⚠
boolector_next_opt ^⚠
boolector_nor ^⚠
boolector_not ^⚠
boolector_one ^⚠
boolector_ones ^⚠
boolector_or ^⚠
boolector_param ^⚠
boolector_parse ^⚠
boolector_parse_btor ^⚠
boolector_parse_btor2 ^⚠
boolector_parse_smt1 ^⚠
boolector_parse_smt2 ^⚠
boolector_pop ^⚠
boolector_print_model ^⚠
boolector_print_stats ^⚠
boolector_push ^⚠
boolector_read ^⚠
boolector_redand ^⚠
boolector_redor ^⚠
boolector_redxor ^⚠
boolector_release ^⚠
boolector_release_all ^⚠
boolector_release_sort ^⚠
boolector_repeat ^⚠
boolector_reset_assumptions ^⚠
boolector_reset_stats ^⚠
boolector_reset_time ^⚠
boolector_rol ^⚠
boolector_roli ^⚠
boolector_ror ^⚠
boolector_rori ^⚠
boolector_saddo ^⚠
boolector_sat ^⚠
boolector_sdiv ^⚠
boolector_sdivo ^⚠
boolector_set_abort ^⚠
boolector_set_msg_prefix ^⚠
boolector_set_opt ^⚠
boolector_set_sat_solver ^⚠
boolector_set_symbol ^⚠
boolector_set_term ^⚠
boolector_set_trapi ^⚠
boolector_sext ^⚠
boolector_sgt ^⚠
boolector_sgte ^⚠
boolector_simplify ^⚠
boolector_slice ^⚠
boolector_sll ^⚠
boolector_slt ^⚠
boolector_slte ^⚠
boolector_smod ^⚠
boolector_smulo ^⚠
boolector_sra ^⚠
boolector_srem ^⚠
boolector_srl ^⚠
boolector_ssubo ^⚠
boolector_sub ^⚠
boolector_terminate ^⚠
boolector_true ^⚠
boolector_uaddo ^⚠
boolector_udiv ^⚠
boolector_uext ^⚠
boolector_uf ^⚠
boolector_uf_assignment ^⚠
boolector_ugt ^⚠
boolector_ugte ^⚠
boolector_ult ^⚠
boolector_ulte ^⚠
boolector_umulo ^⚠
boolector_unsigned_int ^⚠
boolector_urem ^⚠
boolector_usubo ^⚠
boolector_var ^⚠
boolector_version ^⚠
boolector_write ^⚠
boolector_xnor ^⚠
boolector_xor ^⚠
boolector_zero ^⚠

Type Definitions

BoolectorSort
BtorOptBetaReduceMode
BtorOptDPQsort
BtorOptEngine
BtorOptFunEagerLemmas
BtorOptIncrementalSMT1
BtorOptInputFormat
BtorOptJustHeur
BtorOptOutputBase
BtorOptOutputFormat
BtorOptPropPathSel
BtorOptQuantSynth
BtorOptSLSStrat
BtorOptSatEngine
BtorOption
BtorSolverResult